D:dsys{i:l}, w:world{i:l}. possible-world{i:l}(D; w)  Prop{i'} 

latex

Definitions	S  T, t  T, x:A. B(x), Msg, Top
Lemmas	top wf, rcv wf, ma-da wf, eq id wf, ifthenelse wf, mlnk wf, lsrc wf, w-M wf, Msg wf, w-Msg wf, w-m wf, w-withlnk wf